Nuprl Lemma : ecl-trans-halt2_wf
0,22
postcript
pdf
ds
:
x
:Id fp
Type,
da
:
k
:Knd fp
Type,
A
:ecl-trans-tuple{i:l}(
ds
;
da
).
ecl-trans-halt2(
ds
;
da
;
A
)
(event-info(
ds
;
da
) List)
Prop
latex
Definitions
ecl-trans-tuple{i:l}(
ds
;
da
)
,
Knd
,
a
:
A
fp
B
(
a
)
,
x
.
t
(
x
)
,
Id
,
ecl-trans-halt2(
ds
;
da
;
A
)
,
Prop
,
b
,
ecl-trans-h(
v
)
,
ecl-trans-state(
v
;
L
)
,
event-info(
ds
;
da
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Lemmas
nat
wf
,
event-info
wf
,
ecl-trans-state
wf
,
ecl-trans-h
wf
,
assert
wf
,
Id
wf
,
fpf
wf
,
Knd
wf
,
ecl-trans-tuple
wf
origin
ds:x:Id fp
Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da).
(event-info(ds;da) List)Prop ds:x:Id fp Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da).
(event-info(ds;da) List)Prop 
x. t(x)
b